Nuprl Lemma : comb_for_node_wf
4,23
postcript
pdf
(
E
,
x
,
y
,
z
. tree_node(<
x
,
y
>))
E
:Type
Tree(
E
)
Tree(
E
)
True
Tree(
E
)
latex
Definitions
T
,
True
,
Tree(
E
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
tree
wf
,
true
wf
,
squash
wf
,
node
wf
origin
E,x,y,z. tree_node(<x, y>)) 
E:Type
Tree(E)Tree(E)
TrueTree(E) E,x,y,z. tree_node(<x, y>)) E:TypeTree(E)Tree(E)TrueTree(E) T
x:A. B(x) T